\begin{tabbing}
$\forall$$i$,$x$:Id, $k$:Knd, ${\it ds}$:fpf(Id; $x$.Type), $T$:Type, $f$:(decl{-}state(${\it ds}$)$\rightarrow$$T$$\rightarrow$decl{-}type\=\{i:l\}\+
\\[0ex](${\it ds}$; $x$)).
\-\\[0ex]normal{-}ds\=\{i:l\}\+
\\[0ex](${\it ds}$)
\-\\[0ex]$\Rightarrow$ normal{-}type\=\{i:l\}\+
\\[0ex]($T$)
\-\\[0ex]$\Rightarrow$ (($\uparrow$isrcv($k$)) $\Rightarrow$ ($i$ = destination(lnk($k$))))
\\[0ex]$\Rightarrow$ es{-}real\=\{i:l\}\+
\\[0ex](${\it es}$.effect{-}p(${\it es}$; $i$; ${\it ds}$; $k$; $T$; $x$; $f$))
\-
\end{tabbing}